\begin{tabbing}
change{-}to($x$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case TERMOF\{change{-}to{-}lemma2:ObjectId, i:l, i:l\}($T$,${\it eq}$,${\it es}$,$x$,$e$)\+
\\[0ex]o\=f inl($p$) =$>$ inl ($p$.1) \+
\\[0ex]$\mid$ inr($q$) =$>$ inr $\cdot$ 
\-\-
\end{tabbing}